En esta sección detallaremos los aspectos que consideramos mas importantes 
sobre la implementación de la herramienta que exponemos.
En primer lugar, realizaremos un repaso a la arquitectura del sistema y explicaremos los módulos que lo componen.
A continuación veremos cómo es la interacción entre los distintos módulos.

\subsection{Descripción de la arquitectura}

El esquema de ejecución de nuestra herramienta tiene una estructura de pipeline (ver sección \ref{sec:pipeline}). Para su realización, se identificaron los distintos módulos funcionales que conforman la arquitectura del proyecto. Estos módulos están disponibles a través de métodos de acceso, que definen la interfaz del módulo para poder ser utilizado. Este tipo de arquitectura nos permitió dividir y paralelizar de forma clara y simple el
trabajo a realizar, de forma que podíamos ir avanzando en diferentes módulos al mismo tiempo, con el ahorro de tiempo 
que ello suponía. La única dificultad fue definir claramente los métodos de acceso a los módulos, pues los módulos son 
dependientes unos de otros, y a la hora de ensamblarlos deberíamos no tener dificultades. Un esquema de los módulos que 
componen nuestro sistema, y las dependencias entre ellos, se puede ver en la figura \ref{fig:umlmodulos}. 

\begin{figure}[h!]
  \centering
    \includegraphics[width=\textwidth]{umlmodulos}    
    \caption{Diagrama UML de los módulos que componen el sistema y sus dependencias.}
    \label{fig:umlmodulos}
\end{figure}

A continuación realizaremos una descripción de cada módulo, explicando características relevantes de cada uno, y 
mostrando algunos diagramas UML que ayuden a su comprensión.

\subsubsection{Módulo de análisis SQL: SQL\_parser}

Como ya se ha mencionado, nuestra herramienta incorpora un analizador de lenguaje SQL. El objetivo de este analizador no
es comprobar la corrección de las sentencias introducidas, sino generar una estructura C++ que represente las sentencias
SQL dadas a las herramienta, ya se mediante la entrada estándar o mediante un fichero. SQL es un lenguaje con una 
gramática muy amplia, por lo que hemos limitado la gramática que acepta este analizador a un subconjunto representativo de la misma, descrito en la sección \ref{sec:ambito}. No obstante, en futuras versiones de esta herramienta uno de los objetivos marcados es la ampliación de la gramática aceptada. Esta mejora 
dotaría de mayor libertad a los usuarios a la hora de poder seleccionar las tablas o vistas sobre las que obtener 
casos de prueba, sin necesidad de reescribir las sentencias de definición de estas.

Este analizador está implementado mediante la utilización de la herramienta GNU Bison \cite{bison} y Flex \cite{Flex}, y actualmente 
acepta código SQL de definición de bases de datos con las características indicadas en la sección \ref{sec:ambito} exceptuando las consultas de agregación. Consideramos importante la implementación de agregados (GROUP BY, HAVING) con la técnica presentada en \cite{flops2010}, sin embargo esta característica inicialmente planeada ha quedado fuera de la versión actual del prototipo por restricciones de tiempo.

\subsubsection{Módulo para la representación de SQL en C++: SQL\_cpp\_representation}

El objetivo del módulo \emph{SQL parser} es la generación de una estructura que representa las tablas y vistas indicadas
por el usuario. Para ello, creamos un módulo que diera soporte para poder realizar esta representación. Este módulo 
está diseñado con especial cuidado, pues queríamos que fuese extensible de una forma sencilla. Este requerimiento que 
nos impusimos se debe a que la gramática admitida por el analizador de SQL puede extenderse en versiones futuras, por 
lo que se deberían definir nuevas estructuras para su representación en caso de que fuera necesario. En la figura 
\ref{fig:umlestructura} se puede observar un diagrama de clases que componen este módulo.

\begin{figure}[h!]
  \centering
    \includegraphics[width=\textwidth]{umlestructura}
    \caption{Diagrama UML de las clases que componen el módulo para la representación en C++ de tablas, vistas, 
    consultas y expresiones SQL.}
    \label{fig:umlestructura}
\end{figure}

\subsubsection{Módulo para la representación y generación de fórmulas de restricciones: Formula\_representation}

Una vez se ha generado una estructura en C++ que represente las tablas y vistas SQL suministradas por el usuario, el 
objetivo es generar las fórmulas de restricciones sobre la tabla o vista que se indique. Para ello, necesitábamos dar 
soporte para la representación de las fórmulas de restricciones, de forma que fuera lo más fiel a la representación 
descrita en la sección \ref{sec:formulas}, y adoptada de \cite{flops2010}. Con este propósito, decidimos crear el 
módulo \emph{Formula representation}. En la figura \ref{fig:umlformulas} se puede observar un diagrama UML que representa
este módulo.

\begin{figure}[h!]
  \centering
    \includegraphics[width=\textwidth]{umlformulas}
    \caption{Diagrama UML de las clases que componen el módulo para la representación de fórmulas de restricciones.}
    \label{fig:umlformulas}
\end{figure}

Cómo se puede observar, éste módulo incluye una clase \emph{FormulaGenerator}. Esta clase es la encargada de generar la
fórmula de restricciones para una tabla o vista indicada por el usuario. Para generar éstas fórmulas, se ha implementado
el algoritmo de generación de fórmulas descrito en \ref{sec:formula:restricciones}. %Este algoritmo, definido en términos
%matemáticos, es un algoritmo rescursivo, que responde al siguiente pseudocódigo:

%\small{
%\begin{verbatim}
%proc generateFormula(name:string, schema:Schema)
%begin
%      if(schema contains 'name')
%	 if('name' is a table in schema) generate formula for table with name 'name'
%	 else if('name' is a view in schema) 
%		  for each element in from clause
%		      generateFormula(element name,schema)
%		  endfor		  
%		  make the cojunction of all formulas of 'from elements'
%		  compute where condition
		  
%end
%\end{verbatim} 
%}

%Destacar que en este algoritmo no se tratan sentencias SQL de agregación (\cod{GROUP BY}), sin embargo, consideramos su 
%implementación prioritaria para completar la herramienta, siendo uno de los objetivos a corto plazo que nos planteamos.

\subsubsection{Módulo traductor a lenguaje de restricciones de un resolutor específico}

La representación de fórmulas de restricciones que utilizamos es una representación genérica, próxima al lenguaje 
matemático. Esto nos da la posibilidad de poder traducir esa representación a modelos de restricciones que acepten 
resolutores de restricciones concretos. Únicamente bastaría con implementar un nuevo módulo que tome como entrada
un fórmula de restricciones con la representación propia y traducirla al lenguaje concreto. 

El modelo de restricciones, traducido al lenguaje de un resolutor concreto o de un lenguaje de programación de restricciones específico puede ser guardado en un fichero. De esta forma, podríamos ejecutar el resolutor en cuestión, indicando que tome como entrada el fichero guardado. El resolutor asignará 
valores a las variables simbólicas que componen el modelo obteniendo, si existiera, el caso de prueba deseado.

Actualmente, nuestra herramienta realiza la traducción al lenguaje de modelado de restricciones MiniZinc \cite{MiniZinc}. 
Elegimos este lenguaje por ser aceptado por un gran número de resolutores de restricciones. Hemos tenido especial cuidado a la hora de mostrar el resultado 
proporcionado por el resolutor, pues considerábamos útil el hecho de generar sentencias SQL que poblaran las tablas
de la base de datos involucradas en la vista o tabla de la que se buscaba un caso de prueba. Esta sentencias están
introducidas mediante: 

 \begin{verbatim}
  INSERT INTO table_name (atributos) VALUES (valores)
 \end{verbatim}
Esto permitiría ejecutar estas sentencias SQL en el gestor de bases de datos que este utilizando el usuario, y poder así 
ejecutar los casos de prueba.

\subsection{Interacción entre módulos}

A continuación explicaremos distintas secuencias de ejecución que puede tener nuestra herramienta. Para facilitar la comprensión nos
ayudaremos de diagramas de secuencias.

En la figura \ref{fig:secuenciafich} se describe el comportamiento de nuestro sistema cuando la entrada del sistema es un
fichero SQL con sentencias de definición de tablas y vistas (ver apéndice \ref{app:sec:input} para ver un ejemplo de 
fichero de entrada). En este caso, el módulo de análisis de SQL leerá el fichero indicado y creará una estructura C++ que
represente a las tablas y vistas que estén definidas. Al final de este proceso, se preguntará al usuario por una de las
tablas o vistas para la que se quiera generar un caso de prueba, y se comunicará al módulo de generación de fórmulas que genere
una fórmula de restricciones para la tabla o vista indicada. Este módulo preguntará al usuario por el número máximo de filas
que pueden tener las tablas involucradas en la generación de la fórmula de restricciones para la tabla o vista que se indique. 
Una vez que haya generado esta fórmula, se traducirá a un modelo en lenguaje MiniZinc, el cual podrá ser ejecutado 
posteriormente por un resolutor que acepte este lenguaje para obtener un caso de prueba.

\begin{figure}[h!]
  \centering
    \includegraphics[width=\textwidth]{secuenciafich}
    \caption{Diagrama de secuencias con fichero de entrada.}
    \label{fig:secuenciafich}
\end{figure}

En la figura \ref{fig:secuenciainterac} se muestra una fase inicial de interacción con el usuario. En el caso de que el usuario no indique un fichero de entrada en el que se encuentren las definiciones de tablas y vistas, 
se pueden introducir en la herramienta de forma interactiva. Una vez que el usuario ha introducido todas las sentencias SQL de
definición de tablas y vistas, se procederá al análisis de estas, continuando con el mismo proceso que en el caso 
anterior.

\begin{figure}[h!]
  \centering
    \includegraphics[width=\textwidth]{secuenciainterac}
    \caption{Diagrama de secuencias interactivo.}
    \label{fig:secuenciainterac}
\end{figure}

La salida que proporciona nuestra herramienta constituye un modelo MiniZinc válido. Este modelo se puede guardar en un fichero, indicando su ruta con la opción \cod{--output ruta} (ver manual en apéndice \ref{app:manual}) o redirigiendo la salida estándar, para posteriormente obtener sus soluciones a través del resolutor de restricciones. 

